$\forall$$A$:Type, $B$:($A$$\rightarrow$Type), $C$:Type, $D$:($C$$\rightarrow$Type).
\\[0ex]$C$ $\subseteq\rho$ $A$ $\Rightarrow$ ($\forall$$a$:$C$. $B$($a$) $\subseteq\rho$ $D$($a$)) $\Rightarrow$ ($a$:$A$$\rightarrow$$B$($a$)) $\subseteq\rho$ ($c$:$C$$\rightarrow$$D$($c$))